((APPEND (NIL . (DECL (*) (OT& (GROUND GROUND) . GROUND) CONSTANT NIL
INFIX 800) . NIL . ((* . (CONSTANT . ((GROUND GROUND) . GROUND) .
UNIVERSAL . NIL . (1 . * . INFIX . 800 .) . 1 . * .))) . NIL . NIL . NIL .
NIL . NIL . APPEND . NIL . NIL . 1 .) ((((∀ U V)) (= (* U V) (CONDI (NULL
U) V (CONS (CAR U) (* (CDR U) V))))) . (AXIOM (TM& ((∀ U V)) (= (* U V)
(CONDI (NULL U) V (CONS (CAR U) (* (CDR U) V)))))) . NIL . ((CDR LISP . 7)
(CAR LISP . 7) (CONS LISP . 6) (NULL LISP . 8) (V LISP . 1) (U LISP . 1)
(* . 1)) . NIL . NIL . NIL . (2) . NIL . APPEND . NIL . NIL . 2 .) ((((∀ X
U V)) (= (* (CONS X U) V) (CONS X (* U V)))) . (DECSIMP (TM& ((∀ X U V))
(= (* (CONS X U) V) (CONS X (* U V)))) SRIGHT (LR&) (LR&) (LR& (LISP .
12)) (LR& 2 (LISP . 14) (LISP . 15) (LISP . 16))) . NIL . ((* . 1) (V LISP
. 1) (U LISP . 1) (X LISP . 2) (CONS LISP . 6)) . NIL . NIL . NIL . ((LISP
. 16) (LISP . 15) (LISP . 14) 2 (LISP . 12)) . NIL . APPEND . NIL . NIL .
3 .) ((⊃ (∧ (LIST (* NNIL V)) (((∀ X U)) (⊃ (LIST (* U V)) (LIST (* (CONS
X U) V))))) (((∀ U)) (LIST (* U V)))) . (∀E PHI (TM& ((λ U)) (LIST (* U
V))) (LN& LISP . 17) (LR& (LISP . 12))) . NIL . ((V LISP . 1) (* . 1)
(LIST LISP . 9) (CONS LISP . 6) (NNIL LISP . 5) (X LISP . 2) (U LISP . 1))
. NIL . NIL . NIL . ((LISP . 17) (LISP . 12)) . NIL . APPEND . NIL . NIL .
4 .) ((⊃ (((∀ X U)) (⊃ (LIST (* U V)) (LIST (CONS X (* U V))))) (((∀ U))
(LIST (* U V)))) . (REWRITE SRIGHT (LN& . 4) (LR& 3 2 (LISP . 13)) (LR&
(LISP . 12))) . NIL . ((V LISP . 1) (* . 1) (LIST LISP . 9) (CONS LISP .
6) (X LISP . 2) (U LISP . 1)) . NIL . NIL . NIL . ((LISP . 17) (LISP . 16)
(LISP . 15) (LISP . 14) 2 (LISP . 13) (LISP . 12)) . NIL . APPEND . NIL .
NIL . 5 .) ((((∀ U V)) (LIST (* U V))) . (TAUT (TM& ((∀ U V)) (LIST (* U
V))) (LR& 5 (LISP . 12))) . NIL . ((U LISP . 1) (LIST LISP . 9) (* . 1) (V
LISP . 1)) . NIL . NIL . NIL . ((LISP . 12) (LISP . 13) 2 (LISP . 14)
(LISP . 15) (LISP . 16) (LISP . 17)) . NIL . APPEND . NIL . NIL . 6 .)
(NIL . (COMMENTL THE LAST TWO STEPS SHOULD BE DOABLE WITH A SINGLE DECSIMP
BUT I HAVE NOT BEEN ABLE TO DO IT) . NIL . NIL . NIL . NIL . NIL . NIL .
NIL . APPEND . NIL . NIL . 7 .)) (LISP (NIL . (DECL (U V W) (OT& . GROUND)
VARIABLE LIST) . NIL . ((V . (VARIABLE . GROUND . LIST . NIL . NIL . 1 . V
.)) (LIST . (VARIABLE . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . (4 .
LIST . PREFIX . 1000 .) . 1 . LIST .)) (U . (VARIABLE . GROUND . LIST .
NIL . NIL . 1 . U .)) (W . (VARIABLE . GROUND . LIST . NIL . NIL . 1 . W
.))) . NIL . NIL . NIL . NIL . NIL . LISP . NIL . NIL . 1 .) (NIL . (DECL
(X Y Z) (OT& . GROUND) VARIABLE SEXP) . NIL . ((Y . (VARIABLE . GROUND .
SEXP . NIL . NIL . 2 . Y .)) (SEXP . (VARIABLE . ((GROUND) . TRUTHVAL) .
UNIVERSAL . NIL . (4 . SEXP . PREFIX . 1000 .) . 2 . SEXP .)) (X .
(VARIABLE . GROUND . SEXP . NIL . NIL . 2 . X .)) (Z . (VARIABLE . GROUND
. SEXP . NIL . NIL . 2 . Z .))) . NIL . NIL . NIL . NIL . NIL . LISP . NIL
. NIL . 2 .) (NIL . (DECL (A B C) (OT& . GROUND) VARIABLE) . NIL . ((B .
(VARIABLE . GROUND . UNIVERSAL . NIL . NIL . 3 . B .)) (A . (VARIABLE .
GROUND . UNIVERSAL . NIL . NIL . 3 . A .)) (C . (VARIABLE . GROUND .
UNIVERSAL . NIL . NIL . 3 . C .))) . NIL . NIL . NIL . NIL . NIL . LISP .
NIL . NIL . 3 .) (NIL . (DECL (PHI) (OT& (GROUND) . TRUTHVAL) VARIABLE) .
NIL . ((PHI . (VARIABLE . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . NIL .
4 . PHI .))) . NIL . NIL . NIL . NIL . NIL . LISP . NIL . NIL . 4 .) (NIL
. (DECL (NNIL) (OT& . GROUND) CONSTANT LIST) . NIL . ((LIST . 1) (NNIL .
(CONSTANT . GROUND . LIST . NIL . NIL . 5 . NNIL .))) . NIL . NIL . NIL .
NIL . NIL . LISP . NIL . NIL . 5 .) (NIL . (DECL (CONS) (OT& (GROUND
GROUND) . GROUND) CONSTANT) . NIL . ((CONS . (CONSTANT . ((GROUND GROUND)
. GROUND) . UNIVERSAL . NIL . NIL . 6 . CONS .))) . NIL . NIL . NIL . NIL
. NIL . LISP . NIL . NIL . 6 .) (NIL . (DECL (CAR CDR) (OT& (GROUND) .
GROUND) CONSTANT) . NIL . ((CAR . (CONSTANT . ((GROUND) . GROUND) .
UNIVERSAL . NIL . NIL . 7 . CAR .)) (CDR . (CONSTANT . ((GROUND) . GROUND)
. UNIVERSAL . NIL . NIL . 7 . CDR .))) . NIL . NIL . NIL . NIL . NIL .
LISP . NIL . NIL . 7 .) (NIL . (DECL (NULL) (OT& (GROUND) . TRUTHVAL)
CONSTANT) . NIL . ((NULL . (CONSTANT . ((GROUND) . TRUTHVAL) . UNIVERSAL .
NIL . NIL . 8 . NULL .))) . NIL . NIL . NIL . NIL . NIL . LISP . NIL . NIL
. 8 .) (NIL . (DECL (LIST) (OT& (GROUND) . TRUTHVAL) CONSTANT) . NIL .
((LIST . (CONSTANT . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . NIL . 9 .
LIST .))) . NIL . NIL . NIL . NIL . NIL . LISP . NIL . NIL . 9 .) (NIL .
(DECL (SEXP) (OT& (GROUND) . TRUTHVAL) CONSTANT) . NIL . ((SEXP .
(CONSTANT . ((GROUND) . TRUTHVAL) . UNIVERSAL . NIL . NIL . 10 . SEXP .)))
. NIL . NIL . NIL . NIL . NIL . LISP . NIL . NIL . 10 .) ((((∀ U)) (SEXP
U)) . (AXIOM (TM& ((∀ U)) (SEXP U))) . NIL . ((SEXP . 10) (U . 1)) . NIL .
NIL . NIL . (11) . NIL . LISP . NIL . NIL . 11 .) ((((∀ X U)) (LIST (CONS
X U))) . (AXIOM (TM& ((∀ X U)) (LIST (CONS X U)))) . NIL . ((LIST . 9)
(CONS . 6) (X . 2) (U . 1)) . NIL . NIL . NIL . (12) . NIL . LISP . NIL .
NIL . 12 .) ((((∀ U)) (≡ (NULL U) (= U NNIL))) . (AXIOM (TM& ((∀ U)) (≡
(NULL U) (= U NNIL)))) . NIL . ((NULL . 8) (NNIL . 5) (U . 1)) . NIL . NIL
. NIL . (13) . NIL . LISP . NIL . NIL . 13 .) ((((∀ X U)) (¬ (NULL (CONS X
U)))) . (AXIOM (TM& ((∀ X U)) (¬ (NULL (CONS X U))))) . NIL . ((NULL . 8)
(CONS . 6) (X . 2) (U . 1)) . NIL . NIL . NIL . (14) . NIL . LISP . NIL .
NIL . 14 .) ((((∀ X U)) (= (CAR (CONS X U)) X)) . (AXIOM (TM& ((∀ X U)) (=
(CAR (CONS X U)) X))) . NIL . ((CAR . 7) (CONS . 6) (X . 2) (U . 1)) . NIL
. NIL . NIL . (15) . NIL . LISP . NIL . NIL . 15 .) ((((∀ X U)) (= (CDR
(CONS X U)) U)) . (AXIOM (TM& ((∀ X U)) (= (CDR (CONS X U)) U))) . NIL .
((CDR . 7) (CONS . 6) (X . 2) (U . 1)) . NIL . NIL . NIL . (16) . NIL .
LISP . NIL . NIL . 16 .) ((((∀ PHI)) (⊃ (∧ (PHI NNIL) (((∀ X U)) (⊃ (PHI
U) (PHI (CONS X U))))) (((∀ U)) (PHI U)))) . (AXIOM (TM& ((∀ PHI)) (⊃ (∧
(PHI NNIL) (((∀ X U)) (⊃ (PHI U) (PHI (CONS X U))))) (((∀ U)) (PHI U)))))
. NIL . ((CONS . 6) (NNIL . 5) (PHI . 4) (X . 2) (U . 1)) . NIL . NIL .
NIL . (17) . NIL . LISP . NIL . NIL . 17 .)) (COPY (NIL . (DECL (COPY)
(OT& (GROUND) . GROUND) CONSTANT) . NIL . ((COPY . (CONSTANT . ((GROUND) .
GROUND) . UNIVERSAL . NIL . NIL . 1 . COPY .))) . NIL . NIL . NIL . NIL .
NIL . COPY . NIL . NIL . 1 .) ((((∀ U)) (= (COPY U) (CONDI (NULL U) NNIL
(CONS (CAR U) (COPY (CDR U)))))) . (AXIOM (TM& ((∀ U)) (= (COPY U) (CONDI
(NULL U) NNIL (CONS (CAR U) (COPY (CDR U))))))) . NIL . ((U LISP . 1)
(NNIL LISP . 5) (CONS LISP . 6) (CAR LISP . 7) (CDR LISP . 7) (NULL LISP .
8) (COPY . 1)) . NIL . NIL . NIL . (2) . NIL . COPY . NIL . NIL . 2 .) ((⊃
(∧ (= (COPY NNIL) NNIL) (((∀ X U)) (⊃ (= (COPY U) U) (= (COPY (CONS X U))
(CONS X U))))) (((∀ U)) (= (COPY U) U))) . (∀E PHI (TM& ((λ V)) (= (COPY
V) V)) (LN& LISP . 17) (LR& (LISP . 12))) . NIL . ((U LISP . 1) (X LISP .
2) (NNIL LISP . 5) (CONS LISP . 6) (COPY . 1)) . NIL . NIL . NIL . ((LISP
. 17) (LISP . 12)) . NIL . COPY . NIL . NIL . 3 .) ((((∀ X U)) (= (COPY
(CONS X U)) (CONS X (COPY U)))) . (DECSIMP (TM& ((∀ X U)) (= (COPY (CONS X
U)) (CONS X (COPY U)))) SRIGHT (LR&) (LR&) (LR& (LISP . 12)) (LR& 2 (LISP
. 14) (LISP . 15) (LISP . 16))) . NIL . ((COPY . 1) (U LISP . 1) (X LISP .
2) (CONS LISP . 6)) . NIL . NIL . NIL . ((LISP . 16) (LISP . 15) (LISP .
14) 2 (LISP . 12)) . NIL . COPY . NIL . NIL . 4 .) ((((∀ U)) (= (COPY U)
U)) . (DECSIMP (TM& ((∀ U)) (= (COPY U) U)) SRIGHT (LR& 3) (LR&) (LR&
(LISP . 12)) (LR& 2 (LISP . 13) 4)) . NIL . ((COPY . 1) (U LISP . 1)) .
NIL . NIL . NIL . ((LISP . 12) 2 (LISP . 14) (LISP . 15) (LISP . 16) (LISP
. 13) (LISP . 17)) . NIL . COPY . NIL . NIL . 5 .)) (LIST ((((∀ U V)) (=
(* U V) (CONDI (NULL U) V (CONS (CAR U) (* (CDR U) V))))) . (AXIOM (TM&
((∀ U V)) (= (* U V) (CONDI (NULL U) V (CONS (CAR U) (* (CDR U) V)))))) .
NIL . ((* APPEND . 1) (U . (VARIABLE . (VAR& . VTYP1) . UNIVERSAL . NIL .
NIL . 1 . U .)) (V . (VARIABLE . (VAR& . VTYP2) . UNIVERSAL . NIL . NIL .
1 . V .)) (NULL . (VARIABLE . (VAR& . VTYP3) . UNIVERSAL . NIL . NIL . 1 .
NULL .)) (CONS . (VARIABLE . (VAR& . VTYP4) . UNIVERSAL . NIL . NIL . 1 .
CONS .)) (CAR . (VARIABLE . (VAR& . VTYP5) . UNIVERSAL . NIL . NIL . 1 .
CAR .)) (CDR . (VARIABLE . (VAR& . VTYP6) . UNIVERSAL . NIL . NIL . 1 .
CDR .))) . NIL . ((VTYP6 (GROUND) . GROUND) (VTYP3 (GROUND) . TRUTHVAL)
(VTYP2 . GROUND) (VTYP1 . GROUND) (VTYP5 (GROUND) VAR& . VTYP8) (VTYP4
((VAR& . VTYP8) GROUND) VAR& . VTYP10)) . NIL . (1) . NIL . LIST . NIL .
NIL . 1 .)))